Nuprl Lemma : namer-disjoint_wf
11,40
postcript
pdf
n
,
m
:
,
nmr1
:Namer(
n
;[]),
nmr2
:Namer(
m
;[]). namer-disjoint(
n
;
m
;
nmr1
;
nmr2
)
latex
Definitions
,
t
T
,
Id
,
type
List
,
[]
,
f
(
a
)
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
A
,
x
:
A
B
(
x
)
,
{
i
..
j
}
,
Inj(
A
;
B
;
f
)
,
x
:
A
B
(
x
)
,
P
&
Q
,
{
x
:
A
|
B
(
x
)}
,
Type
,
s
=
t
,
,
namer-disjoint(
n1
;
n2
;
nmr1
;
nmr2
)
,
Namer(
n
;
Id_list
)
Lemmas
int
seg
wf
,
inject
wf
,
Id
wf
,
not
wf
,
l
member
wf
,
nat
wf
origin
n, m:
, nmr1:Namer(n;[]), nmr2:Namer(m;[]). namer-disjoint(n;m;nmr1;nmr2) 
n, m:, nmr1:Namer(n;[]), nmr2:Namer(m;[]). namer-disjoint(n;m;nmr1;nmr2) Tx:A. B(x) l)
A
B(x)
}
B(x)